/*!
 * \file set_relation_test_ops.cc
 *
 * \brief Set and Relation operations tests
 *
 * This file is to test all of the Set and Relation operations
 *
 * \date Started: 12/21/10
 * \date Last Modified: 12/21/10
 * \authors Alan LaMielle
 * \authors Ian Craig
 */

#include <iegenlib/iegenlib.h>

#include <gtest/gtest.h>
#include<iostream>
using std::cout;
using std::endl;

using iegenlib::OperatorEqualsException;
using iegenlib::UnionException;
using iegenlib::ApplyException;
using iegenlib::ComposeException;

using iegenlib::IEGenLibContext;
using iegenlib::Set;
using iegenlib::Relation;
using iegenlib::SRConjunction;
using iegenlib::Symbolic;

/******************************** Set Tests ***********************************/
/********** Equality/Inequality Tests **********/
TEST(EqualityTest, SetContext){
  IEGenLibContext context1,context2;
  context1.setSimplifyConjunctions(false);
  ASSERT_NE(context1,context2);

  Set PS1("{[a]: a>10 and a<15 and a<14}",context1);
  Set PS2("{[a]: a>10 and a<15 and a<14}",context1);
  Set PS3("{[b]: b>10 and b<15 and b<14}",context2);

  //Testing for equality with the same contexts is ok
  ASSERT_EQ(PS1,PS2);

  //Testing for equality with different contexts is not allowed
  bool fail=true;
  try{
    PS1==PS3;
  }catch(OperatorEqualsException e){
    fail=false;
  }
  if(fail){
    ADD_FAILURE()<<"OperatorEqualsException not raised";
  }
}

TEST(EqualityTest, Set1){
  Set PS1("{[a,b]: a=b}");
  Set PS2("{[a,b]: a=b}");

  EXPECT_TRUE(PS1 == PS2);

  Set PS3("{[x,y]: x=y}");

  EXPECT_TRUE(PS1 == PS3);

  Set PS4("{[x,y]: y=x}");

  EXPECT_TRUE(PS1 == PS4);

  Set PS5("{[x,y,z]: x=y}");

  EXPECT_FALSE(PS1 == PS5);
}

TEST(EqualityTest, Set2){
  Set PS6("{[x,y]: f(x)=f(y)}");
  Set PS7("{[a,b]: f(a)=f(b)}");
  Set PS10("{[a,b]: g(a)=g(b)}");

  EXPECT_TRUE(PS6 == PS7);
  EXPECT_FALSE(PS7 == PS10);
}

TEST(EqualityTest, Set3){
  IEGenLibContext context;
  context.addSymbolic(Symbolic("x"));
  context.addSymbolic(Symbolic("y"));

  Set PS8("{[a,b]: a=b}", context);
  Set PS9("{[a,b]: a=b}", context);

  EXPECT_TRUE(PS8 == PS9);
}

TEST(EqualityTest, Set4){
  Set PS11("{[a,1]: a=0}");
  Set PS12("{[a,1]: a=0}");
  Set PS13("{[a,2]: a=0}");
  Set PS14("{[1,a]: a=0}");

  EXPECT_TRUE(PS11 == PS12);
  EXPECT_FALSE(PS11 == PS13);
  EXPECT_FALSE(PS11 == PS14);
}

TEST(EqualityTest, Set5){
  IEGenLibContext context;
  context.setSimplifyConjunctions(false);
  Set PS6("{[x,y]: f(x)=f(y)}",context);
  Set PS15("{[a,b]: c=0}",context);

  string exp = "fail";
  try{
    PS6 == PS15;
  }catch(OperatorEqualsException e){
    exp = e.what();
  }
  EXPECT_EQ(exp, "Cannot use == on sets with existential variables.");

  exp = "fail";
  try{
    PS15 == PS6;
  }catch(OperatorEqualsException e){
    exp = e.what();
  }
  EXPECT_EQ(exp, "Cannot use == on sets with existential variables.");
}

TEST(EqualityTest, Set6){
  Set PS16("{[a,b]: a>b}");
  Set PS17("{[a,b]: a>b}");
  Set PS18("{[a,b]: a<b}");

  EXPECT_TRUE(PS16 == PS17);
  EXPECT_FALSE(PS16 == PS18);
}

TEST(EqualityTest, Set7){
  Set PS19("{[a,b]: a=10}");
  Set PS20("{[ba,aa]: ba=10}");
  EXPECT_EQ(PS19 , PS20);
}

TEST(InequalityTest, Set1){
  Set PS1("{[a,b]: a=b}");
  Set PS2("{[a,b]: a=b+3}");
  set<SRConjunction> S1 (PS1.conSetBegin(), PS1.conSetEnd());
  set<SRConjunction> S2 (PS2.conSetBegin(), PS2.conSetEnd());
  EXPECT_TRUE(S2 < S1);//a-b-0 vs a-b-3

  Set PS3("{[x,y]: x=y and x=3}");
  set<SRConjunction> S3 (PS3.conSetBegin(), PS3.conSetEnd());
  EXPECT_TRUE(S1 < S3);

  Set PS4("{[x,y]: y<x}");
  set<SRConjunction> S4 (PS4.conSetBegin(), PS4.conSetEnd());
  EXPECT_TRUE(S4 < S1);//eq first 0 vs 1

  Set PS5("{[x,y,z]: x=y and x<4}");
  set<SRConjunction> S5 (PS5.conSetBegin(), PS5.conSetEnd());
  EXPECT_FALSE(S3 < S5);//eq first 2 vs 1
}

TEST(InequalityTest, Set2){
  Set PS6("{[x,y]: f(x)=f(y) and x=5}");
  Set PS7("{[a,b]: f(a)=f(b) and a=4}");
  Set PS10("{[a,b]: g(a)=g(b)}");
  set<SRConjunction> S6 (PS6.conSetBegin(), PS6.conSetEnd());
  set<SRConjunction> S7 (PS7.conSetBegin(), PS7.conSetEnd());
  set<SRConjunction> S10 (PS10.conSetBegin(), PS10.conSetEnd());
  EXPECT_TRUE(S6 < S7);//x-4 vs x-5
  EXPECT_FALSE(S10 < S10);
}

TEST(InequalityTest, Set3){
  IEGenLibContext context;
  context.addSymbolic(Symbolic("x"));
  context.addSymbolic(Symbolic("y"));

  Set PS8("{[a,b]: a=b}", context);
  Set PS9("{[a,b]: a=b}", context);
  Set PS16("{[a,b]: a=b and x=y}", context);
  set<SRConjunction> S8 (PS8.conSetBegin(), PS8.conSetEnd());
  set<SRConjunction> S9 (PS9.conSetBegin(), PS9.conSetEnd());
  EXPECT_FALSE(S8 < S9);
  set<SRConjunction> S16 (PS16.conSetBegin(), PS16.conSetEnd());
  EXPECT_TRUE(S8 < S16);
}

TEST(InequalityTest, Set4){
  Set PS11("{[a,1]: a=1}");
  Set PS12("{[a,1]: a=0}");
  Set PS13("{[a,2]: a=0}");
  Set PS14("{[1,a]: a=0}");

  set<SRConjunction> S11 (PS11.conSetBegin(), PS11.conSetEnd());
  set<SRConjunction> S12 (PS12.conSetBegin(), PS12.conSetEnd());
  set<SRConjunction> S13 (PS13.conSetBegin(), PS13.conSetEnd());
  set<SRConjunction> S14 (PS14.conSetBegin(), PS14.conSetEnd());
  EXPECT_FALSE(S12 < S11);
  EXPECT_TRUE(S11 < S13);
  EXPECT_FALSE(S14 < S11);

  Set PS15("{[a,b]: c=1}");
  set<SRConjunction> S15 (PS15.conSetBegin(), PS15.conSetEnd());

  EXPECT_TRUE(S15 < S11);
}
/***********************************************/


/********** Union Tests **********/
//test that makes sure the conjunction size increases to 2 after the union
TEST(UnionTest, SetConCountUnion){
   Set PS1("{[x,y,z]:a<b and a<c}");

   Set PS2("{[s,a,d]:a<b and a<c}");

   Set PS3 = PS1.Union(PS2);
   EXPECT_EQ(PS3.conSize(), 1);
}

TEST(UnionTest, SetContext){
  IEGenLibContext context1,context2;
  context1.setSimplifyConjunctions(false);
  ASSERT_NE(context1,context2);

  Set PS1("{[a]: a>10 and a<15 and a<14}",context1);
  Set PS2("{[a]: a>10 and a<15 and a<14}",context1);
  Set PS3("{[b]: b>10 and b<15 and b<14}",context2);

  //Union with the same contexts is ok
  Set PS4(PS1.Union(PS2));

  //Union with different contexts is not allowed
  bool fail=true;
  try{
    Set PS5(PS1.Union(PS3));
  }catch(UnionException e){
    fail=false;
  }
  if(fail){
    ADD_FAILURE()<<"UnionException not raised";
  }
}

TEST(UnionTest, set1){
  Set s1("{[k]: k > 10}");
  Set s2("{[i]: i > 10}");

  Set s3(s1.Union(s2));
  EXPECT_EQ(s3.get_isl(), "{[k] : k-11>=0}");
  EXPECT_TRUE(s3==s1);
}

TEST(UnionTest, set12){
  Set s1("{[k]: k > 10}");
  Set s2("{[k]: k > 3}");

  Set s3(s1.Union(s2));

  EXPECT_EQ(s3.get_isl(), "{[k] : k-11>=0; [k] : k-4>=0}");
}

TEST(UnionTest, set2){
  try{
    Set s1("{[k,t]: k > l}");
    Set s2("{[i]: j > i}");

    Set s3(s1.Union(s2));
  }catch(UnionException e){
//    std::cout<<e.what()<<std::endl;
    return;//success
  }
  ADD_FAILURE()<<"Union Exception not raised";
}

TEST(UnionTest, set3){
  try{
    Set s1("{[3]: k > l}");
    Set s2("{[i]: j > i}");

    Set s3(s1.Union(s2));
  }catch(UnionException e){
//    std::cout<<e.what()<<std::endl;
    return;//success
  }
  ADD_FAILURE()<<"Union Exception not raised";
}

TEST(UnionTest, doubleUnion){
    Set s1("{[k]: k > 7}");
    Set s2("{[k]: k > 4}");

    Set s3(s1.Union(s2));
    EXPECT_EQ(s3.get_isl(), "{[k] : k-8>=0; [k] : k-5>=0}");
    Set s4("{[i]: i>j}");
    Set s5(s3.Union(s4));
    Set s_expected("{[k] : exists(j : k-8>=0); [k] : exists(j : k-5>=0); [k] : exists(j : k-j-1>=0)}");
    EXPECT_EQ(s5, s_expected);
}

TEST(UnionTest, CrazydoubleUnionUnion){
//need to get these changed to testing ==
    Set s1("{[k]: k > 7}");
    Set s2("{[k]: k > 4}");

    Set s3(s1.Union(s2));
    EXPECT_EQ(s3.get_isl(), "{[k] : k-8>=0; [k] : k-5>=0}");
    Set s4("{[i]: i>j}");
    Set s5("{[i]: i<j}");
    Set s6(s5.Union(s4));
    Set s6_expected("{[i] : exists(j : -i+j-1>=0); [i] : exists(j : i-j-1>=0)}");
    EXPECT_EQ(s6, s6_expected);
    EXPECT_EQ(s6.get_isl(), "{[i]}");
    Set s7(s3.Union(s6));
    Set s7_expected(
      "{[k] : exists(j : k-8>=0); [k] : exists(j : k-5>=0); [k] : exists(j : -k+j-1>=0); [k] : exists(j : k-j-1>=0)}");
    EXPECT_EQ(s7, s7_expected);
    EXPECT_EQ(s7.get_isl(), "{[k]; [k] : k-8>=0; [k] : k-5>=0}");
    Set s8(s5.Union(s3.Union(s4)));
    Set s8_expected(
      "{[i] : exists(j : i-8>=0); [i] : exists(j : i-5>=0); [i] : exists(j : -i+j-1>=0); [i] : exists(j : i-j-1>=0)}");
    EXPECT_EQ(s8, s8_expected);
    EXPECT_EQ(s8.get_isl(), "{[i]; [i] : i-8>=0; [i] : i-5>=0}");
    Set s9(s6.Union(s3));
    Set s9_expected(
      "{[i] : exists(j : i-8>=0); [i] : exists(j : i-5>=0); [i] : exists(j : -i+j-1>=0); [i] : exists(j : i-j-1>=0)}");
    EXPECT_EQ(s9, s9_expected);
    EXPECT_EQ(s9.get_isl(), "{[i]; [i] : i-8>=0; [i] : i-5>=0}");
}
/*********************************/


/********** Apply Tests **********/
TEST(ApplyTest, SetContext){
  IEGenLibContext context1,context2;
  context1.setSimplifyConjunctions(false);
  ASSERT_NE(context1,context2);

  Set PS1("{[a]: a>10 and a<15 and a<14}",context1);
  Relation PR2("{[a]->[b]: a>10 and a<15 and a<14}",context1);
  Relation PR3("{[b]->[c]: b>10 and b<15 and b<14}",context2);

  //Apply with the same contexts is ok
  Set PS4(PR2.Apply(PS1));

  //Apply with different contexts is not allowed
  bool fail=true;
  try{
    Set PS5(PR3.Apply(PS1));
  }catch(ApplyException e){
    fail=false;
  }
  if(fail){
    ADD_FAILURE()<<"ApplyException not raised";
  }
}

TEST(ApplyTest, test1){
  Set r1("{[s] : s >= 0 and s<10}");
  Relation r2("{[a]->[b,c] : a=b and c=2a}");

  Set PS3(r2.Apply(r1));

  EXPECT_EQ(PS3.get_isl(), "{[b,c] : 2b-c=0 and b>=0 and -b+9>=0}");
}

TEST(ApplyTest, test2){
  try{
    Set r1("{[s,q] : s >= 0 and s<10}");
    Relation r2("{[a]->[b,c] : a=b and c=2a}");

    Set PS3(r2.Apply(r1));

  }catch(ApplyException e){
//    std::cout<<e.what()<<std::endl;
    return;//success
  }
  ADD_FAILURE()<<"Compose Exception not raised";
}

TEST(ApplyTest, test3){
  Set r1("{[3] : s >= 0 and s<10}");
  Relation r2("{[a]->[b,c] : a=b and c=2a}");

  Set PS3(r2.Apply(r1));

  Set PS3_expected("{[b,c] : exists(s : c-6=0 and b-3=0 and s>=0 and -s+9>=0)}");
  EXPECT_EQ(PS3, PS3_expected);
  EXPECT_EQ(PS3.get_isl(), "{[b,c] : c-6=0 and b-3=0}");
}

TEST(ApplyTest, test4){
  Set r1("{[x,e,s] : s >= 0 and s<10}");
  Relation r2("{[a,3,g]->[b,c] : a=b and c=2a}");

  Set PS3(r2.Apply(r1));

  Set PS3_expected("{[b,c] : exists(s : 2b-c=0 and s>=0 and -s+9>=0)}");
  EXPECT_EQ(PS3, PS3_expected);
  EXPECT_EQ(PS3.get_isl(), "{[b,c] : 2b-c=0}");
}

TEST(ApplyTest, test5){
  Set r1("{[s,4] : s >= 0 and s<10}");
  Relation r2("{[a,5]->[b,c] : a=b and c=2a}");

  Set PS3(r2.Apply(r1));

  Set PS3_expected("{[b,c] : 1=0}");
  EXPECT_EQ(PS3, PS3_expected);
  EXPECT_EQ(PS3.get_isl(), "{[b,c] : 1=0}");
}

TEST(ApplyTest, test6){
  Set r1("{[s,5] : s >= 0 and s<10}");
  Relation r2("{[a,5]->[b,c] : a=b and c=2a and f(c)=q}");

  Set PS3(r2.Apply(r1));

  EXPECT_EQ(PS3.get_isl(), "{[b,c] : 2b-c=0 and b>=0 and -b+9>=0}");
}

TEST(ApplyTest, test7){
  Set r1("{[a,5] : a >= 0 and a<10}");
  Relation r2("{[a,5]->[b,c] : a=b and c=2a and f(c)=q}");

  Set PS3(r2.Apply(r1));

  EXPECT_EQ(PS3.get_isl(), "{[b,c] : 2b-c=0 and b>=0 and -b+9>=0}");
}
/*********************************/
/******************************************************************************/

/******************************** Relation Tests ******************************/
/********** Equality Tests **********/
TEST(EqualityTest, RelationContext){
  IEGenLibContext context1,context2;
  context1.setSimplifyConjunctions(false);
  ASSERT_NE(context1,context2);

  Relation PR1("{[a]->[c]: a>10 and a<15 and a<14}",context1);
  Relation PR2("{[a]->[c]: a>10 and a<15 and a<14}",context1);
  Relation PR3("{[b]->[c]: b>10 and b<15 and b<14}",context2);

  //Testing for equality with the same contexts is ok
  ASSERT_EQ(PR1,PR2);

  //Testing for equality with different contexts is not allowed
  bool fail=true;
  try{
    PR1==PR3;
  }catch(OperatorEqualsException e){
    fail=false;
  }
  if(fail){
    ADD_FAILURE()<<"OperatorEqualsException not raised";
  }
}

TEST(EqualityTest, Relation1){
  Relation PS1("{[a]->[b]: a=b}");
  Relation PS2("{[a]->[b]: a=b}");

  EXPECT_TRUE(PS1 == PS2);

  Relation PS3("{[x]->[y]: x=y}");

  EXPECT_TRUE(PS1 == PS3);

  Relation PS4("{[x]->[y]: y=x}");

  EXPECT_TRUE(PS1 == PS4);

  Relation PS5("{[x]->[y,z]: x=y}");

  EXPECT_FALSE(PS1 == PS5);
}

TEST(EqualityTest, Relation2){
  Relation PS6("{[x]->[y]: f(x)=f(y)}");
  Relation PS7("{[a]->[b]: f(a)=f(b)}");
  Relation PS10("{[a]->[b]: g(a)=g(b)}");

  EXPECT_TRUE(PS6 == PS7);
  EXPECT_FALSE(PS7 == PS10);
}

TEST(EqualityTest, Relation3){
  IEGenLibContext context;
  context.addSymbolic(Symbolic("x"));
  context.addSymbolic(Symbolic("y"));

  Relation PS8("{[a]->[b]: a=b}", context);
  Relation PS9("{[a]->[b]: a=b}", context);

  EXPECT_TRUE(PS8 == PS9);
}

TEST(EqualityTest, Relation4){
  Relation PS11("{[a]->[1]: a=0}");
  Relation PS12("{[a]->[1]: a=0}");
  Relation PS13("{[a]->[2]: a=0}");
  Relation PS14("{[1]->[a]: a=0}");

  EXPECT_TRUE(PS11 == PS12);
  EXPECT_FALSE(PS11 == PS13);
  EXPECT_FALSE(PS11 == PS14);
}

TEST(EqualityTest, Relation5){
  IEGenLibContext context;
  context.setSimplifyConjunctions(false);
  Relation PS6("{[x]->[y]: f(x)=f(y)}",context);
  Relation PS15("{[a]->[b]: c=0}",context);
  string exp = "fail";
  try{
    PS6 == PS15;
  }catch(OperatorEqualsException e){
    exp = e.what();
  }
  EXPECT_EQ(exp, "Cannot use == on relations with existential variables.");

  exp = "fail";
  try{
    PS15 == PS6;
  }catch(OperatorEqualsException e){
    exp = e.what();
  }
  EXPECT_EQ(exp, "Cannot use == on relations with existential variables.");
}

TEST(EqualityTest, Relation6){
  Relation PS16("{[a]->[b]: a>b}");
  Relation PS17("{[a]->[b]: a>b}");
  Relation PS18("{[a]->[b]: a<b}");

  EXPECT_TRUE(PS16 == PS17);
  EXPECT_FALSE(PS16 == PS18);

  Relation PS19("{[b]->[a]: a>b}");

  EXPECT_FALSE(PS16 == PS19);
}

TEST(InequalityTest, Relation1){
  Relation PS1("{[a]->[b]: a=b}");
  Relation PS2("{[a]->[b]: a=b+3}");
  set<SRConjunction> S1 (PS1.conSetBegin(), PS1.conSetEnd());
  set<SRConjunction> S2 (PS2.conSetBegin(), PS2.conSetEnd());
  EXPECT_FALSE(S1 < S2);

  Relation PS3("{[x]->[y]: x=y}");
  set<SRConjunction> S3 (PS3.conSetBegin(), PS3.conSetEnd());
  EXPECT_TRUE(S2 < S3);

  Relation PS4("{[x]->[y]: y=x-4}");
  set<SRConjunction> S4 (PS4.conSetBegin(), PS4.conSetEnd());
  EXPECT_TRUE(S4 < S1);

  Relation PS5("{[x]->[y,z]: x=y}");
  set<SRConjunction> S5 (PS5.conSetBegin(), PS5.conSetEnd());
  EXPECT_TRUE(S1 < S5);//looks at the exp vec size
}

TEST(InequalityTest, Relation2){
  Relation PS6("{[x]->[y]: f(x)=f(y)+1}");
  Relation PS7("{[a]->[b]: f(a)=f(b)}");
  Relation PS10("{[a]->[b]: g(a)=g(b)}");
  set<SRConjunction> S6 (PS6.conSetBegin(), PS6.conSetEnd());
  set<SRConjunction> S7 (PS7.conSetBegin(), PS7.conSetEnd());
  set<SRConjunction> S10 (PS10.conSetBegin(), PS10.conSetEnd());
  EXPECT_TRUE(S6 < S7);
  EXPECT_FALSE(S7 < S10);
}

TEST(InequalityTest, Relation3){
  IEGenLibContext context;
  context.addSymbolic(Symbolic("x"));
  context.addSymbolic(Symbolic("y"));

  Relation PS8("{[a]->[b]: a=b}", context);
  Relation PS9("{[a]->[b]: a=b}", context);
  Relation PS16("{[a]->[b]: a=b and x=y}", context);
  set<SRConjunction> S9 (PS9.conSetBegin(), PS9.conSetEnd());
  set<SRConjunction> S8 (PS8.conSetBegin(), PS8.conSetEnd());
  set<SRConjunction> S16 (PS16.conSetBegin(), PS16.conSetEnd());
  EXPECT_FALSE(S8 < S9);
  EXPECT_TRUE(S8 < S16);
}

TEST(InequalityTest, Relation4){
  IEGenLibContext context;
  context.addSymbolic(Symbolic("x"));
  context.addSymbolic(Symbolic("y"));

  Relation PS11("{[a]->[1]: a=1}",context);
  Relation PS12("{[a,b]->[1]: a=0}",context);
  Relation PS13("{[a]->[2]: a=0}",context);
  Relation PS14("{[1]->[a]: a=0}",context);
  set<SRConjunction> S12 (PS12.conSetBegin(), PS12.conSetEnd());
  set<SRConjunction> S13 (PS13.conSetBegin(), PS13.conSetEnd());
  set<SRConjunction> S14 (PS14.conSetBegin(), PS14.conSetEnd());
  set<SRConjunction> S11 (PS11.conSetBegin(), PS11.conSetEnd());
  EXPECT_TRUE(S11 < S12);
  EXPECT_FALSE(S13 < S11);
  EXPECT_FALSE(S12 < S14);

  Relation PS15("{[a]->[b]: c=-3}",context);
  Relation PS1("{[a]->[b]: a=b}",context);
  set<SRConjunction> S1 (PS1.conSetBegin(), PS1.conSetEnd());
  set<SRConjunction> S15 (PS15.conSetBegin(), PS15.conSetEnd());
  Relation PS16("{[a]->[b]: a=b and x=y}", context);
  set<SRConjunction> S16 (PS16.conSetBegin(), PS16.conSetEnd());
  EXPECT_TRUE(S1 < S16);
}
/************************************/


/********** Union Tests **********/
TEST(UnionTest, RelationContext){
  IEGenLibContext context1,context2;
  context1.setSimplifyConjunctions(false);
  ASSERT_NE(context1,context2);

  Relation PR1("{[a]->[b]: a>10 and a<15 and a<14}",context1);
  Relation PR2("{[a]->[b]: a>10 and a<15 and a<14}",context1);
  Relation PR3("{[b]->[c]: b>10 and b<15 and b<14}",context2);

  //Union with the same contexts is ok
  Relation PR4(PR1.Union(PR2));

  //Union with different contexts is not allowed
  bool fail=true;
  try{
    Relation PR5(PR1.Union(PR3));
  }catch(UnionException e){
    fail=false;
  }
  if(fail){
    ADD_FAILURE()<<"UnionException not raised";
  }
}

TEST(UnionTest, Rel1){
  Relation PS1("{[x]->[y]: y>10}");
  Relation PS2("{[x]->[y]: x>10}");
  Relation PS4("{[x]->[y] : y-11>=0; [x]->[y] : x-11>=0}");
  Relation PS3(PS1.Union(PS2));

  EXPECT_EQ(PS3==PS4, true);

  PS3 = PS2.Union(PS1);

  EXPECT_EQ(PS3==PS4, true);
}

TEST(UnionTest, Rel12){
  Relation PS1("{[x]->[y]: y>10}");
  Relation PS2("{[x]->[y]: y>10}");

  Relation PS3(PS1.Union(PS2));

  EXPECT_EQ(PS3.get_isl(), "{[x]->[y] : y-11>=0}");
  EXPECT_TRUE(PS3==PS1);

  PS3 = PS2.Union(PS1);

  EXPECT_EQ(PS3.get_isl(), "{[x]->[y] : y-11>=0}");
  EXPECT_TRUE(PS3==PS1);
}

TEST(UnionTest, Rel2){
  try{
    Relation PS1("{[x]->[y]: a < 0}");
    Relation PS2("{[y]->[z,t]: b > 0}");

    Relation PS3(PS1.Union(PS2));
  }catch(UnionException e){
//    std::cout<<e.what()<<std::endl;
    return;//success
  }
  ADD_FAILURE()<<"Union Exception not raised";
}

TEST(UnionTest, Rel3){
  try{
    Relation PS1("{[x]->[y]: a < 0}");
    Relation PS2("{[y]->[z,t]: b > 0}");

    Relation PS3(PS2.Union(PS1));
  }catch(UnionException e){
//    std::cout<<e.what()<<std::endl;
    return;//success
  }
  ADD_FAILURE()<<"Union Exception not raised";
}

TEST(UnionTest, Rel4){
  try{
    Relation PS1("{[x,t,2]->[y,r,u]: a < 0}");
    Relation PS2("{[y,r,e]->[z,w,q]: b > 0}");

    Relation PS3(PS1.Union(PS2));

  }catch(UnionException e){
//    std::cout<<e.what()<<std::endl;
    return;//success
  }
  ADD_FAILURE()<<"Union Exception not raised";
}

TEST(UnionTest, Rel5){
    Relation PS1("{[x,y,z]->[a,c]: a < 0}");
    Relation PS2("{[w,d,r]->[z,t]: b > 0}");

    Relation PS3(PS1.Union(PS2));
    Relation PS_expected("{[x,y,z]->[a,c] : exists(b : -a-1>=0); [x,y,z]->[a,c] : exists(b : b-1>=0)}");
    EXPECT_EQ(PS3, PS_expected);
    EXPECT_EQ(PS3.get_isl(), "{[x,y,z]->[a,c]; [x,y,z]->[a,c] : -a-1>=0}");
}

TEST(UnionTest, Rel6){
  Relation r1("{[x,y,2]->[l,r] : x > 0}");
  Relation r11("{[x,y,5]->[l,r] : x < 0}");
  Relation r112(r1.Union(r11));
  EXPECT_EQ(r112.get_isl(), "{[x,y,5]->[l,r] : -x-1>=0; [x,y,2]->[l,r] : x-1>=0}");
}
/*********************************/


/********** Inverse Tests **********/
//tests that the conjucntion size is 1
TEST(InverseTest, RelationInverseConCount){
   Relation PR2("{[x,x,x]->[a,b,c]}");
   PR2.Inverse();
   EXPECT_EQ(PR2.conSize(), 1);

   Relation PR3("{[x,x,x]->[y,y,y]}");
   Relation PR3new=PR3.Inverse();
   EXPECT_EQ(PR3new.conSize(), 1);
}

TEST(InverseTest, test1){
  Relation PR1("{[x,y,z]->[a,b,c]}");
  Relation PR1new=PR1.Inverse();
  EXPECT_EQ(PR1new.get_isl(), "{[a,b,c]->[x,y,z]}");
}

TEST(InverseTest, test2){
  Relation PR2("{[x,x,x]->[a,b,c]}");
  Relation PR2new=PR2.Inverse();
  EXPECT_EQ(PR2new.get_isl(), "{[a,b,c]->[x,x1,x2] : x-x1=0 and x-x2=0}");
}

TEST(InverseTest, test3){
  Relation PR3("{[x,x,x]->[y,y,y]}");
  Relation PR3new=PR3.Inverse();
  EXPECT_EQ(PR3new.get_isl(),
    "{[y,y1,y2]->[x,x1,x2] : y-y1=0 and y-y2=0 and x-x1=0 and x-x2=0}");
}

TEST(InverseTest, test4){
  Relation PR10("{[x,x,x]->[y,y,y]: x = 0}");
  Relation PR10new=PR10.Inverse();

  Relation PR10_expected(
    "{[y,y1,y2]->[x,x1,x2] : y-y1=0 and y-y2=0 and x-x1=0 and x-x2=0 and x=0}");
  EXPECT_EQ(PR10new, PR10_expected);
  EXPECT_EQ(PR10new.get_isl(),
    "{[y,y1,y2]->[x,x1,x2] : y-y1=0 and y-y2=0 and x2=0 and x1=0 and x=0}");
}

TEST(InverseTest, test5){
  Relation PR4("{[a]->[b,c]}");
  Relation PR5("{[b,c]->[a]}");
  EXPECT_TRUE(PR4.Inverse() == PR5);
}

TEST(InverseTest, test6){
  Relation PR6("{[a]->[b,1]}");
  Relation PR7("{[b,1]->[a]}");
  EXPECT_TRUE(PR6.Inverse() == PR7);
}

TEST(InverseTest, test7){
  Relation PR8("{[a]->[b,c]: a = 0}");
  Relation PR9("{[b,c]->[a]: a = 0}");
  EXPECT_TRUE(PR8.Inverse() == PR9);
}

TEST(InverseTest, test8){
  Relation PR11("{[a]->[b,c]: f(a) = 0}");
  Relation PR12("{[b,c]->[a]: f(a) = 0}");
  EXPECT_TRUE(PR11.Inverse() == PR12);
}

TEST(InverseTest, test9){
  Relation PR13("{[a]->[b,1]: a = 0}");
  Relation PR14("{[b,1]->[a]: a = 0}");
  EXPECT_TRUE(PR13.Inverse() == PR14);
}

TEST(InverseTest, test10){
  Relation PR15("{[a]->[]: a = 0}");
  Relation PR16("{[]->[a]: a = 0}");
  EXPECT_TRUE(PR15.Inverse() == PR16);
  EXPECT_EQ(PR15.Inverse().get_isl(), "{[]->[a] : a=0}");
}
/***********************************/


/********** Compose Tests **********/
TEST(ComposeTest, RelationContext){
  IEGenLibContext context1,context2;
  context1.setSimplifyConjunctions(false);
  ASSERT_NE(context1,context2);

  Relation PR1("{[a]->[b]: a>10 and a<15 and a<14}",context1);
  Relation PR2("{[a]->[b]: a>10 and a<15 and a<14}",context1);
  Relation PR3("{[b]->[c]: b>10 and b<15 and b<14}",context2);

  //Compose with the same contexts is ok
  Relation PR4(PR1.Compose(PR2));

  //Compose with different contexts is not allowed
  bool fail=true;
  try{
    Relation PR5(PR1.Compose(PR3));
  }catch(ComposeException e){
    fail=false;
  }
  if(fail){
    ADD_FAILURE()<<"ComposeException not raised";
  }
}

TEST(ComposeTest, test1){
  Relation PS1("{[a]->[b]: a < 0}");
  Relation PS2("{[y]->[z]: y > 0}");

  Relation PS3(PS1.Compose(PS2));

  Relation PS_expected("{[y]->[b] : exists(z : -z-1>=0 and y-1>=0)}");
  EXPECT_EQ(PS3, PS_expected);
  EXPECT_EQ(PS3.get_isl(), "{[y]->[b] : y-1>=0}");

  PS3 = PS2.Compose(PS1);

  Relation PS3_expected("{[a]->[z] : exists(y : -a-1>=0 and y-1>=0)}");
  EXPECT_EQ(PS3, PS3_expected);
  EXPECT_EQ(PS3.get_isl(), "{[a]->[z] : -a-1>=0}");
}

TEST(ComposeTest, test2){
 Relation r1("{[k]->[l] : k > l}");
 Relation r2("{[i]->[j] : j > i}");
 Relation r3(r1.Compose(r2));

 Relation r3_expected("{[i]->[l] : exists(k : -i+k-1>=0 and -l+k-1>=0)}");
 EXPECT_EQ(r3, r3_expected);
 EXPECT_EQ(r3.get_isl(), "{[i]->[l]}");
}

TEST(ComposeTest, test3){
  Relation PS1("{[x]->[y]: a < 0}");
  Relation PS2("{[y]->[z]: b > 0}");

  Relation PS3(PS1.Compose(PS2));

  Relation PR_expected("{[y]->[y1] : exists(a,b : -a-1>=0 and b-1>=0)}");
  EXPECT_EQ(PS3, PR_expected);
  EXPECT_EQ(PS3.get_isl(), "{[y]->[y1]}");

  PS3 = PS2.Compose(PS1);
  
  Relation PR3_expected("{[x]->[z] : exists(a,b : -a-1>=0 and b-1>=0)}");
  EXPECT_EQ(PS3, PR3_expected);
  EXPECT_EQ(PS3.get_isl(), "{[x]->[z]}");
}

TEST(ComposeTest, test4){
 try{
   Relation r1("{[k]->[l,r] : k > l}");
   Relation r2("{[i]->[j,d] : j > i}");

   Relation PS3(r1.Compose(r2));

  }catch(ComposeException e){
//    std::cout<<e.what()<<std::endl;
    return;//success
  }
  ADD_FAILURE()<<"Compose Exception not raised";
}

TEST(ComposeTest, test5){
  Relation r1("{[x,y,2]->[l,r] : x > 0}");
  Relation r2("{[c,d,e]->[q,s,5]}");

  Relation PS3(r1.Compose(r2));

  EXPECT_EQ(PS3.get_isl(), "{[c,d,e]->[l,r] : 1=0}");
}


TEST(ComposeTest, test6){
  Relation r1("{[x,y,2]->[l,r] : x > 0}");
  Relation r11("{[x,y,5]->[l,r] : x < 0}");
  Relation r112(r1.Union(r11));
  EXPECT_EQ(r112.get_isl(), "{[x,y,5]->[l,r] : -x-1>=0; [x,y,2]->[l,r] : x-1>=0}");

  Relation r2("{[c,d,e]->[q,s,5]}");

  Relation PS3(r112.Compose(r2));

  Relation PR3_expected("{[c,d,e]->[l,r] : exists(x : -x-1>=0)}");
  EXPECT_EQ(PS3, PR3_expected);
  EXPECT_EQ(PS3.get_isl(), "{[c,d,e]->[l,r]}");
}


TEST(ComposeTest, test7){
  Relation r1("{[x,y,2]->[l,r,6] : x > 0}");
  Relation r11("{[x,y,5]->[l,r,6] : x < 0}");
  Relation r112(r1.Union(r11));
  EXPECT_EQ(r112.get_isl(), "{[x,y,5]->[l,r,6] : -x-1>=0; [x,y,2]->[l,r,6] : x-1>=0}");

  Relation r2("{[c,d,e]->[q,s,5]}");

  Relation PS3(r112.Compose(r2));

  Relation PR3_expected("{[c,d,e]->[l,r,6] : exists(x : -x-1>=0)}");
  EXPECT_EQ(PS3, PR3_expected);
  EXPECT_EQ(PS3.get_isl(), "{[c,d,e]->[l,r,6]}");
}

TEST(ComposeTest, test8){
  Relation r1("{[a,b]->[n,l] : a > l}");
  Relation r2("{[i,j]->[c,d] : j > i}");
  Relation R3("{[a,b]->[n,l] : a-l-1>=0; [a,b]->[n,l] : b-a-1>=0}");
  Relation r3(r1.Union(r2));

  EXPECT_TRUE(r3==R3);

  Relation r4("{[s,t]->[r] : r>10}");

  Relation r5(r4.Compose(r3));

  Relation PR5_expected("{[a,b]->[r] : exists(t : r-11>=0 and -a+b-1>=0); [a,b]->[r] : exists(t : r-11>=0 and a-t-1>=0)}");
  EXPECT_EQ(r5, PR5_expected);
  EXPECT_EQ(r5.get_isl(), "{[a,b]->[r] : r-11>=0; [a,b]->[r] : r-11>=0 and -a+b-1>=0}");
}

TEST(ComposeTest, test9){
  Relation r1("{[x,y,2]->[l,r,6] : x > 0}");
  Relation r2("{[c,d,e]->[q,s,t]}");

  Relation PS3(r1.Compose(r2));

  Relation PR3_expected("{[c,d,e]->[l,r,6] : exists(x : x-1>=0)}");
  EXPECT_EQ(PS3, PR3_expected);
  EXPECT_EQ(PS3.get_isl(), "{[c,d,e]->[l,r,6]}");
}

TEST(ComposeTest, test10){
  Relation r1("{[a,b]->[4,l] : a > l}");
  Relation r2("{[i,j]->[c,d] : j > i}");

  Relation r5(r2.Compose(r1));

  Relation PR5_expected("{[a,b]->[c,d] : exists(l : l-5>=0 and a-l-1>=0)}");
  EXPECT_EQ(r5, PR5_expected);
  EXPECT_EQ(r5.get_isl(), "{[a,b]->[c,d] : a-6>=0}");
}

TEST(ComposeTest, test11){
  IEGenLibContext context;
  context.setSimplifyConjunctions(false);
  Relation r1("{[y,y,2]->[r,r] : y > 0}",context);
  Relation r2("{[c,d,e]->[s,s,2]}",context);

  Relation PS3(r1.Compose(r2));

  EXPECT_EQ(PS3.get_isl(), "{[c,d,e]->[r,r1] : exists(s,s1,y,y1 : y-y1=0 and s1-y1=0 and s-s1=0 and s-y=0 and r-r1=0 and y-1>=0)}");
}

TEST(ComposeTest, test12){
  Relation r1("{[]->[r,r] : y > 0}");
  Relation r2("{[c,d,e]->[]}");

  Relation PS3(r1.Compose(r2));
  Relation PR4("{[c,d,e]->[r,r1] : r-r1=0 and y-1>=0}");

  Relation PR3_expected("{[c,d,e]->[r,r1] : exists(y : r-r1=0 and y-1>=0)}");
  EXPECT_EQ(PS3, PR3_expected);
  EXPECT_EQ(PS3.get_isl(), "{[c,d,e]->[r,r1] : r-r1=0}");
}

TEST(ComposeTest, test13){
  IEGenLibContext context;
  context.setSimplifyConjunctions(false);
  Relation r1("{[a,b]->[]}",context);
  Relation r2("{[]->[c,d]}",context);

  Relation PS3(r1.Compose(r2));

  EXPECT_EQ(PS3.get_isl(), "{[]->[] : exists(a,b,c,d : b-d=0 and a-c=0)}");
}

TEST(ComposeTest, test14){
  Relation r1("{[]->[r,r]}");
  Relation r2("{[c,d,e]->[]}");

  Relation PR3(r1.Compose(r2));
  Relation PR4("{[c,d,e]->[r,r1] : r-r1=0}");

  EXPECT_TRUE(PR3 == PR4);
}

TEST(ComposeTest, test15){
  //{[a]->[b]} compose {[c]->[6]} = {[c]->[b]: a=6}
  Relation r1("{[a]->[b]: a=b}");
  Relation r2("{[c]->[6]}");

  Relation r3(r1.Compose(r2));

  EXPECT_EQ(r3.get_isl(), "{[c]->[b] : b-6=0}");

}
/***********************************/
/******************************************************************************/
